A:Type, B:(AType), eq:EqDecider(A), f1, g1, f2, g2:a:A fp B(a).
f2 || g1  f1  g1  f2  g2  f1  f2  g1  g2 

latex

Definitions	t  T, x(s), x:A. B(x), x. t(x), Top, a:A fp B(a), f  g, x  dom(f), b, f(x), A c B, P  Q, f  g, EqDecider(T), f || g, {T}, P  Q, P & Q, P  Q, P  Q, False, A, b, , , Unit
Lemmas	fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, fpf-join-dom, fpf-sub wf, fpf-compatible wf, fpf wf, deq wf, assert wf, fpf-dom wf, fpf-join wf, top wf, fpf-trivial-subtype-top